COMMENT ⊗   VALID 00006 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	wisc[w86,jmc]		Course description and facts
C00004 00003	possible dates
C00006 00004	∂17-Jan-86  1346	IAM  	i put a photo on your desk   
C00008 00005	Title: Proving properties of programs
C00011 00006	Bio's
C00013 ENDMK
C⊗;
wisc[w86,jmc]		Course description and facts

COMMENT ⊗   VALID 00005 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	possible dates
C00004 00003	∂17-Jan-86  1346	IAM  	i put a photo on your desk   
C00006 00004	Title: Proving properties of programs
C00009 00005	Bio's
C00011 ENDMK
C⊗;
possible dates
july7 OS,DB,KB so far
july14   logic pgm cnf
july21   European AI Brighton
july 28
aug 4   LISP conf MIT aug 4-6
aug 11   symbolic alg conf, aaai phila
aug 18
aug 25 (bad - week near labor day weekend)?

send 
    course description
    bio jmc,clt
    pictures b&w
to
Joleen barnhill
WICS
PO Box 12238
Magalia, CA 95954

916 8730575
by monday

title:
proving properties of programs

ian status?
  guest lect or third instructor
ask ian if he want to participate


jmc
wics

Be sure to find out if you have
any unlisted meetings the week of 
July 11 or July 29 or Aug 18
The lisp conference is Aug 4-6

∂17-Jan-86  1346	IAM  	i put a photo on your desk   
and i will look at der over the weekend.
ian mason

IAM  	
i put a photo on your desk   

thanks
we also will need a brief `bio'.  You can type yours
into the file once I get the course description and John's
and my bios typed in.


ian
wics

Could you send a note to
    Joleen barnhill
    WICS
    PO Box 12238
    Magalia, Ca 95954
telling her what your visa status is and who she should
contact to arrange paying you for the course this summer.
She thought perhaps you would have to be paid through Stanford
instead of directly by WICS.
(her phone is 916 873-0575)

Title: Proving properties of programs

Course description: 

This course will cover formal and informal methods for proving properties
of Lisp-like programs.  We begin with pure Lisp and then present
extensions that allow treating function and control abstractions as first
class objects and allow proving properties of operations that modify data
structures.

The topics include

⊗ representation of pure Lisp programs as functions or partial functions
  in a first order theory,
⊗ extensional properties of programs represented as sentences in the theory
⊗ induction schemas including the minimization schema,
⊗ search strategies represented as functionals -- 
   tools for programming and proving properties of programs 
   that search tree structured spaces,
⊗ properties of and operations on streams,
⊗ proving properties of programs that include escape and co-routine mechanisms,
⊗ notions of equivalence for Lisp list structures (including cyclic structures)
⊗ equations satisfied by programs that modify list structures
⊗ programs for traversing and copying arbitrary list structures 

Text: Selected chapters from LISP: programming and proving
(Stanford course notes, to be published as a book), and reprints.

For whom: mathematicians, computer scientists, professional programmers 
interested in developing skills to reason about programs 
in order to design better programs and eliminate much of the
program debugging effort by improved understanding of high level
programming tools.

Prerequisite: Elementary LISP programming and elementary mathematical
logic including quantifiers.
Bio's

John McCarthy has been Professor of Computer Science at Stanford
since 1962.  His main research is in artificial intelligence and
in mathematical theory of computation.  He invented the LISP programming
language and developed methods for representing such applicative
programs as sentences in mathematical logic and proving their properties.

Dr. Carolyn Talcott is Research Associate in Computer
Science at Stanford.  Her interests include formal reasoning,
mathematical theory of computation, and the application of
theory to the design of programming systems.
Recent work includes developing a model of computation
in which both intensional and extensional properties of programs can be
treated.

Ian Mason is a graduate student in philosophy at Stanford.  His recent
work includes a theory of cyclic list structures and programs that
compute with them.  This includes the LISP rplac operations that don't
fit in the simple theory of pure LISP.